/*
   Copyright (c) 2011 Mizar Tools Contributors (mizartools.org)

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*/
/*  Contributors :
 *	2011-02-04 Marco Riccardi - initial implementation
 *
 */
package org.mizartools.system.utility;

import java.util.HashMap;

import org.mizartools.system.ClusterRegistrationKind;
import org.mizartools.system.ListArticleFile;

public class UniqueIdentifier {

	private static final int ARTICLE_POSITION = 262144; // 2^18 
	private static final int TYPE_POSITION = 8192;		// 2^13 

	private static HashMap<Integer, UniqueIdentifier> hashMapUniqueIdentifier = new HashMap<Integer, UniqueIdentifier>();
	
	public final String aid;
	public final UniqueIdentifierType type;
	public final int nr;
	private String string;
	public int id;
	
	private UniqueIdentifier(String aid, UniqueIdentifierType type, int nr) throws UniqueIdentifierException {
		if (aid == null || type == null || nr < 1 || nr >= TYPE_POSITION) {
			throw new UniqueIdentifierException();
		}
		this.aid = aid;
		this.type = type;
		this.nr = nr;
		if (ListArticleFile.getAllArticleMap().containsKey(aid.toLowerCase())) {
			int i = ListArticleFile.getAllArticleMap().get(aid.toLowerCase()) * ARTICLE_POSITION;
			i = i + type.getId() * TYPE_POSITION;
			i = i + nr;
			this.id = i;
		} else {
			throw new UniqueIdentifierException();
		}
		string = aid + ":" + type + " " + nr;
		if (hashMapUniqueIdentifier.containsKey(this.id)) throw new UniqueIdentifierException();
	};
	
	@Override
	public int hashCode() {
		final int prime = 31;
		int result = 1;
		result = prime * result + id;
		return result;
	}

	@Override
	public boolean equals(Object obj) {
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		UniqueIdentifier other = (UniqueIdentifier) obj;
		if (id != other.id)
			return false;
		return true;
	}

	public String toString(){
		return string;
	}

	public static UniqueIdentifier getInstance(
			String aid, UniqueIdentifierType type, int nr) throws UniqueIdentifierException {
		int id;
		if (aid == null || type == null || nr < 1 || nr >= TYPE_POSITION) {
			throw new UniqueIdentifierException();
		}
		if (ListArticleFile.getAllArticleMap().containsKey(aid.toLowerCase())) {
			int i = ListArticleFile.getAllArticleMap().get(aid.toLowerCase()) * ARTICLE_POSITION;
			i = i + type.getId() * TYPE_POSITION;
			i = i + nr;
			id = i;
		} else {
			throw new UniqueIdentifierException();
		}
		if (!hashMapUniqueIdentifier.containsKey(id)) {
			UniqueIdentifier uniqueIdentifier = new UniqueIdentifier(aid, type, nr);
			hashMapUniqueIdentifier.put(uniqueIdentifier.id, uniqueIdentifier);
		} 
		return hashMapUniqueIdentifier.get(id);
	}

	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature, 
	        org.mizartools.system.xml.Typ typ) throws UniqueIdentifierException {
		int nr = typ.getNr();
		String aid = typ.getAid();
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (typ.getKind()){
				case M : 
					if (nr > signatureItem.nrM) nr = nr - signatureItem.nrM;
					else aid = signatureItem.articleId;
					break;
				case G : 
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				case L : 
					if (nr > signatureItem.nrL) nr = nr - signatureItem.nrL;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (typ.getKind()){
		case M : type = UniqueIdentifierType.mode; break;
		case G : type = UniqueIdentifierType.struct; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature,
			org.mizartools.system.xml.Adjective adjective) throws UniqueIdentifierException {
		org.mizartools.system.xml.Adjective.Kind kind = adjective.getKind();
		if (kind == null) kind = org.mizartools.system.xml.Adjective.Kind.V;
		int nr = adjective.getNr();
		String aid = adjective.getAid();
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (kind){
				case V :
					if (nr > signatureItem.nrV) nr = nr - signatureItem.nrV;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (kind){
		case V : type = UniqueIdentifierType.attr; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature,
			org.mizartools.system.xml.Func func) throws UniqueIdentifierException {
		int nr = func.getNr();
		String aid = func.getAid();
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (func.getKind()){
				case K :
					if (nr > signatureItem.nrK) nr = nr - signatureItem.nrK;
					else aid = signatureItem.articleId;
					break;
				case G : 
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				case U :
					if (nr > signatureItem.nrU) nr = nr - signatureItem.nrU;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (func.getKind()){
		case K : type = UniqueIdentifierType.func; break;
		case G : type = UniqueIdentifierType.aggr; break;
		case U : type = UniqueIdentifierType.sel; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature,
			String aid,
			org.mizartools.system.xml.Constructor.Kind kind, 
			Integer redefnr) throws UniqueIdentifierException {
		int nr = redefnr;
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (kind){
				case M :
					if (nr > signatureItem.nrM) nr = nr - signatureItem.nrM;
					else aid = signatureItem.articleId;
					break;
				case K :
					if (nr > signatureItem.nrK) nr = nr - signatureItem.nrK;
					else aid = signatureItem.articleId;
					break;
				case G : 
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				case R :
					if (nr > signatureItem.nrR) nr = nr - signatureItem.nrR;
					else aid = signatureItem.articleId;
					break;
				case V :
					if (nr > signatureItem.nrV) nr = nr - signatureItem.nrV;
					else aid = signatureItem.articleId;
					break;
				case L :
					if (nr > signatureItem.nrL) nr = nr - signatureItem.nrL;
					else aid = signatureItem.articleId;
					break;
				case U :
					if (nr > signatureItem.nrU) nr = nr - signatureItem.nrU;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (kind){
		case M : type = UniqueIdentifierType.mode; break;
		case K : type = UniqueIdentifierType.func; break;
		case G : type = UniqueIdentifierType.aggr; break;
		case R : type = UniqueIdentifierType.pred; break;
		case V : type = UniqueIdentifierType.attr; break;
		case L : type = UniqueIdentifierType.struct; break;
		case U : type = UniqueIdentifierType.sel; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature,
			String aid,
			org.mizartools.system.xml.Definiens.Constrkind kind, 
			Integer redefnr) throws UniqueIdentifierException {
		int nr = redefnr;
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (kind){
				case M :
					if (nr > signatureItem.nrM) nr = nr - signatureItem.nrM;
					else aid = signatureItem.articleId;
					break;
				case K :
					if (nr > signatureItem.nrK) nr = nr - signatureItem.nrK;
					else aid = signatureItem.articleId;
					break;
				case G : 
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				case R :
					if (nr > signatureItem.nrR) nr = nr - signatureItem.nrR;
					else aid = signatureItem.articleId;
					break;
				case V :
					if (nr > signatureItem.nrV) nr = nr - signatureItem.nrV;
					else aid = signatureItem.articleId;
					break;
				case L :
					if (nr > signatureItem.nrL) nr = nr - signatureItem.nrL;
					else aid = signatureItem.articleId;
					break;
				case U :
					if (nr > signatureItem.nrU) nr = nr - signatureItem.nrU;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (kind){
		case M : type = UniqueIdentifierType.mode; break;
		case K : type = UniqueIdentifierType.func; break;
		case G : type = UniqueIdentifierType.aggr; break;
		case R : type = UniqueIdentifierType.pred; break;
		case V : type = UniqueIdentifierType.attr; break;
		case L : type = UniqueIdentifierType.struct; break;
		case U : type = UniqueIdentifierType.sel; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}
	
	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature,
			String aid,
			org.mizartools.system.xml.Pattern.Kind kind, 
			Integer redefnr) throws UniqueIdentifierException {
		int nr = redefnr;
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (kind){
				case M :
					if (nr > signatureItem.nrM) nr = nr - signatureItem.nrM;
					else aid = signatureItem.articleId;
					break;
				case K :
					if (nr > signatureItem.nrK) nr = nr - signatureItem.nrK;
					else aid = signatureItem.articleId;
					break;
				case G : 
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				case R :
					if (nr > signatureItem.nrR) nr = nr - signatureItem.nrR;
					else aid = signatureItem.articleId;
					break;
				case V :
					if (nr > signatureItem.nrV) nr = nr - signatureItem.nrV;
					else aid = signatureItem.articleId;
					break;
				case L :
					if (nr > signatureItem.nrL) nr = nr - signatureItem.nrL;
					else aid = signatureItem.articleId;
					break;
				case U :
					if (nr > signatureItem.nrU) nr = nr - signatureItem.nrU;
					else aid = signatureItem.articleId;
					break;
				case J :
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (kind){
		case M : type = UniqueIdentifierType.modenot; break;
		case K : type = UniqueIdentifierType.funcnot; break;
		case G : type = UniqueIdentifierType.aggrnot; break;
		case R : type = UniqueIdentifierType.prednot; break;
		case V : type = UniqueIdentifierType.attrnot; break;
		case L : type = UniqueIdentifierType.structnot; break;
		case U : type = UniqueIdentifierType.selnot; break;
		case J : type = UniqueIdentifierType.forgnot; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}
	
	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature, 
			org.mizartools.system.xml.Field field) throws UniqueIdentifierException {
		int nr = field.getNr();
		String aid = field.getAid();
		org.mizartools.system.xml.Field.Kind kind = field.getKind();
		if (kind == null) kind = org.mizartools.system.xml.Field.Kind.U;
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (kind){
				case U :
					if (nr > signatureItem.nrU) nr = nr - signatureItem.nrU;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (kind){
		case U : type = UniqueIdentifierType.sel; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature, String aid,
			org.mizartools.system.xml.Pattern.Constrkind constrkind, 
			Integer constrnr) throws UniqueIdentifierException {
		int nr = constrnr;
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (constrkind){
				case M :
					if (nr > signatureItem.nrM) nr = nr - signatureItem.nrM;
					else aid = signatureItem.articleId;
					break;
				case K :
					if (nr > signatureItem.nrK) nr = nr - signatureItem.nrK;
					else aid = signatureItem.articleId;
					break;
				case G : 
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				case R :
					if (nr > signatureItem.nrR) nr = nr - signatureItem.nrR;
					else aid = signatureItem.articleId;
					break;
				case V :
					if (nr > signatureItem.nrV) nr = nr - signatureItem.nrV;
					else aid = signatureItem.articleId;
					break;
				case L :
					if (nr > signatureItem.nrL) nr = nr - signatureItem.nrL;
					else aid = signatureItem.articleId;
					break;
				case U :
					if (nr > signatureItem.nrU) nr = nr - signatureItem.nrU;
					else aid = signatureItem.articleId;
					break;
				case J :
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (constrkind){
		case M : type = UniqueIdentifierType.mode; break;
		case K : type = UniqueIdentifierType.func; break;
		case G : type = UniqueIdentifierType.aggr; break;
		case R : type = UniqueIdentifierType.pred; break;
		case V : type = UniqueIdentifierType.attr; break;
		case L : type = UniqueIdentifierType.struct; break;
		case U : type = UniqueIdentifierType.sel; break;
		case J : type = UniqueIdentifierType.forg; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature, String aid, 
			org.mizartools.system.xml.Pred.Kind kind,
			Integer nr) throws UniqueIdentifierException {
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (kind){
				case R :
					if (nr > signatureItem.nrR) nr = nr - signatureItem.nrR;
					else aid = signatureItem.articleId;
					break;
				case V :
					if (nr > signatureItem.nrV) nr = nr - signatureItem.nrV;
					else aid = signatureItem.articleId;
					break;
				case P :
					if (nr > signatureItem.nrR) nr = nr - signatureItem.nrR;
					else aid = signatureItem.articleId;
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (kind){
		case R : type = UniqueIdentifierType.pred; break;
		case V : type = UniqueIdentifierType.attr; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(
			AbstractSignature abstractSignature, String aid,
			org.mizartools.system.xml.Func.Kind kind, Integer nr) throws UniqueIdentifierException {
		if (aid == null){
			for (SignatureItem signatureItem : abstractSignature.getSignatureItemList()){
				switch (kind){
				case K :
					if (nr > signatureItem.nrK) nr = nr - signatureItem.nrK;
					else aid = signatureItem.articleId;
					break;
				case G : 
					if (nr > signatureItem.nrG) nr = nr - signatureItem.nrG;
					else aid = signatureItem.articleId;
					break;
				case U :
					if (nr > signatureItem.nrU) nr = nr - signatureItem.nrU;
					else aid = signatureItem.articleId;
					break;
				case F :
					break;
				default :
					throw new UniqueIdentifierException();
				}
				if (aid != null) break;
			}
		}
		UniqueIdentifierType type = null;
		switch (kind){
		case K : type = UniqueIdentifierType.func; break;
		case G : type = UniqueIdentifierType.aggr; break;
		case U : type = UniqueIdentifierType.sel; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(
			RegistrationsSignature registrationSignature, 
			String aid,
			ClusterRegistrationKind clusterRegistrationKind,
			Integer clusterRegistrationNr) throws UniqueIdentifierException {
		UniqueIdentifierType type = null;
		switch (clusterRegistrationKind){
		case condreg : type = UniqueIdentifierType.condreg; break;
		case exreg : type = UniqueIdentifierType.exreg; break;
		case funcreg : type = UniqueIdentifierType.funcreg; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, clusterRegistrationNr);
	}

	public static UniqueIdentifier getInstance(
			TheoremsSignature theoremsSignature,
			String aid, 
			org.mizartools.system.xml.Theorem.Kind kind, 
			Integer nr) throws UniqueIdentifierException {
		UniqueIdentifierType type = null;
		switch (kind){
		case D : type = UniqueIdentifierType.def; break;
		case T : type = UniqueIdentifierType.th; break;
		default :
			throw new UniqueIdentifierException();
		}
		return getInstance(aid, type, nr);
	}

	public static UniqueIdentifier getInstance(String string) throws UniqueIdentifierException {
		int position = string.indexOf(":");
		if (position == -1) {
			throw new UniqueIdentifierException();
		}
		String aid = string.substring(0, position);
		string = string.substring(position+1, string.length());
		position = string.indexOf(" ");
		if (position == -1) {
			throw new UniqueIdentifierException();
		}
		UniqueIdentifierType type = null;
		int nr;
		try{
			type = UniqueIdentifierType.valueOf(string.substring(0, position));
			nr = Integer.parseInt(string.substring(position+1, string.length()));
		}
		catch(Exception e){
			System.err.println(string);
			throw new UniqueIdentifierException();
		} 
		return getInstance(aid, type, nr);
	}

}
